Section 4. The Language of the Strategies

Frequently the user of a theorem prover "knows" a lot of detail about

the  problem  domain  being axiomatized.   Much  of  this information

(almost by definiton) is  domain-dependent and  thus doesn't  fit the

usual set  of strategies as  well as could  be desired. Also  much of

this information is  heuristic in nature   and would be  difficult to

express in the form of  axioms.  To help with these problems  we have

introduced two new ideas:  (1) a language for  describing strategies;

and (2) new data types added to LISP so that the user may tailor-make

his own prover.

The strategy language  allows Boolean expressions over  properties of

clauses.  Major extensions of this idea are contemplated..

The  programmable aspects  allow the  user to  describe   first order

statements, strategies and pattern matching in an intuitive notation.

With these facilities inside LISP we can write new rules of inference

and domain dependent theorem provers.



4-I.  THE CHOICE STRATEGIES.

Choice strategies occur in the following context: Given two  possible

candidates,C1  and  C2,  for  the application  of  a  binary  rule of

inference I, a choice strategy will determine whether not we  wish to

form I(C1,C2).

Builtin choice strategies.

a) NONE  allows unrestricted applications of the rules of inference.

b) ANCESTRY implements the AFF  strategy; that is, to apply  I either

C1 or C2 must be an initial clauses, or, either C1 must appear in the

derivation tree of C2, or C2 must appear in the tree of C1.

c)  SUPPORT  designates the  set-of-support  strategy.  This strategy

basically says that every first-level deduction must have one  of its

parents in the support set.  SUPPORT must be followed by  an argument

list describing which  statements are to be supported.   The elements

of the argument list may either be clause numbers or names  which the

user has associated with certain input clauses.

Example: SUPPORT[1,2,AXIOM[2],THEOREM]  would put clauses  numbered 1

and 2, the  clause AXIOM[2], and all  clauses with name,  THEOREM, in

the support set.

d) VINE strategy says that either C1 or C2 must be an initial clause.

This strategy is known to be incomplete, but is useful in many cases.

e)  UNIT  strategy says  that  either C1  or  C2  are singletons(unit

clauses).  Again, this strategy is  not complete, but is useful  as a



"quick-kill"  or "end-game"  strategy.  It  is easy  to show  that if

there is a UNIT-refutation  then there is a VINE-form  refutation. It

is also easy  to show that if  all the initial statements  are either

units(singletons) or are of the form L1∧L2∧...∧Ln ⊃ M then there is a

UNIT proof.

f)  P1 is  the P1-deduction  of Robinson.  Here it  is  required that

either  C1 or  C2 contain  only positive  literals. This  strategy is

complete.

g) MODEL is the implementation  of a very simple  case of  the model-

relative deduction strategy of Luckham.  Model-relative  deduction is

a generalization of P1 deduction and is complete.  Deduction relative

to a model says that at least one of the clauses C1 or C2 be false of

the  model.   MODEL  expects an  argument  list  describing  a binary

partition of the predicate letters appearing in the  initial clauses.

In the current  restricted implementation this  says either C1  or C2

must have zero  intersection with the  two members of  the partition.

For example, MODEL[;<all  predicate letter occurring in  problem>] is

equivalent  to P1-deduction;  MODEL[P,=;R] defines  a  partition with

positive occurrences of P and =, and negative occurrences of R.

h) DEFMODEL  can be  used to designate  a LISP  function to  define a

model for the current  set of statements.  DEFMODEL expects  a single

argument which is  the name of a  LISP function(of one  argument) and

which implements the defining conditions of a model. The use  of this

strategy requires knowledge of the representation of clauses.



i) EQUALITY signals that the replacement rule, paramodulation,  is to

be  used.   EQUALITY needs  two  arguments: a  predicate  name  to be

interpreted as equality; and  second, a number, called  PDEPTH, which

determines how deep  in the nesting  of function symbols  the matcher

will look in attempting to  match terms.  For example, a PDEPTH  of 1

says only examine primary occurences of terms.



4-II. EDITING STRATEGIES.

Editing  strategies  are  applied  to the  results  of  the  rules of

inference.   These strategies  are used  to  filter  out some  of the

deductions which a rule of inference has generated.

Builtin editing strategies.

a)  DEMOD  is  a  rule  of  simplification  most  commonly   used  in

conjunction  with  EQUALITY.  DEMOD takes  two  arguments.  The first

describes a list of equality units; the second, a number named DDEPTH

which,like PDEPTH, determines a bound on the matching routines.

b) DEPTH takes a single integer argument interpreted to be a bound on

the depth of  function symbol nesting which  must not be  exceeded if

the deduction is to be retained.

For example, DEPTH[4].

c) LENGTH  also takes an  integer argument and  gives a bound  on the

number of literals which will be allowed in any deduction.

d)  SELDEPTH  takes   function  symbol-number  pairs   as  arguments.

SELDEPTH is  a refinement  of DEPTH  in that  the allowable  depth of

nesting of  each function symbol  is determined by  the corresponding

number.

e) Any  of the  primitive constructs of  the pattern  language: TREE,

LENGTH, DEPTH, or OCR.  For example if OCR[f(e,e)] were to  appear in

an editing strategy then  any clauses which contained  "f(e,e)" would

be rejected.



4-III. COMBINING PRIMITIVE STRATEGIES.

Boolean  combinations  of  built-in  or  user-defined  strategies are

allowed.   For example,  a reasonable  choice strategy   is: ancestry

filter form with a set of support being the negation of the statement

to be proved.  This can be written as:

 ANCESTRY ∧ SUPPORT[THEOREM];

An editing strategy which filters out all clauses whose length(number

of literals) is  greater than 4 or  whose depth( depth of  nesting of

function symbols) is greater than 3 can be expressed as:

LENGTH[4] ∨ DEPTH [3];

See the Appendix (A-II) for the rules of combination.



4-IV. THE AUTOMATIC STRATEGY SELECTION.

A very simple  procedure is used to  select the strategies  in PROVE-

mode.   The choice  strategies are  ANCESTRY and,  if  THEOREMNAME is

present as  an axiom  name ,then  SUPPORT[<value of  THEOREMNAME>] is

also used.  Also, if  an equality predicate letter is  declared, then

equality replacement witha  depth bound of 4 is added.

The  editing strategies  are determined  by the  maximum  lengths and

depths which occur in the input clauses.  If equality is present then

a simplification list consisting of all the positive units is used.

The strategy  settings are  automatically changed  if the  program is

terminated without finding a proof.



Section 5. Theorem proving primitives.

It  is now  possible to  write LISP-like  programs which  control the

actions of  the theorem  prover and  manipulate clauses.   Data types

for CLAUSES, STRATEGIES, and PATTERNS have been added to LISP so that

the user can describe  his clause manipulations in the  same notation

which is used  to drive the  on-line prover.  LISP  functions, TRYTIL

and FIND, have been defined to perform controlled  proof-attempts and

clause-list searching.

1. Data Types.

a) [CLAUSES <clauses>] is used  to introduce new clause lists  to the

program.  For example: (SETQ X [CLAUSES DSK:FOO])  when executed will

assign to X the  clauselist manufactured from the statements  on file

FOO.

b)   [CHOICE  <strategy>]   and  [EDIT   <strategy>]   introduce  the

appropriate strategies.

c) [PATTERN <pattern>] is  useful in conjunction with FIND  to filter

out  clauses which match <pattern>.

2. Procedures.

(TRYTIL         <clauses><choice-strategy><edit-strategy><termination

condition>)

where:
1) <clauses> is a list of clauses .

2) <choice-strategy> is a representation of a choice strategy.

3) <edit-strategy> represents an editing strategy.



4) <termination  condition> is  a functional  argument which  will be

evaluated periodically during the  execution of the TRYTIL.   As long

as the condition evaluated to NIL the proof attempt will continue. If

the condition becomes  true then TRYTIL will  return the list  of all

deductions which have been made.

For example:

(TRYTIL [CLAUSES  DSK: FOO] [CHOICE  ANCESTRY∧SUPPORT[THEOREM]] [EDIT

LENGTH[4]∨DEPTH[3]] (FUNCTION (LAMBDA()(GREATERP LEVEL 3))) )

will begin  a proof  search using file  DSK:FOO with  choice strategy

being AFF  and supporting  the negation  of the  theorem.  Deductions

whose length is greater than 4 or whose depth of function  nesting is

greater than 3 will be discarded.  The proof search will terminate at

the end of level 3.

If a refutation is discovered during any attempt, (QED)  is returned.

If no refutation is found, then the on-line editor is called  to give

the user a chance to examine the current proof environment.  There is

a third  way to exit  TRYTIL: since the  on-line editor  is available

inside the  proof attempt,  typing ABandon  <clauses> to  the  editor

will  force termination  of  the proof  attempt and  will  return the

selected <clauses>.

(FIND <clauses><pattern>)

where:  1)  <clauses>  is  a list  of  clauses.   2)  <pattern>  is a

condition which is to be applied to each element of <clauses>.



The  value of  FIND is  a  list of  all elements  of  <clauses> which

satisfy the <pattern>.



Section 6. The Answer Extractor.

A subset of the Luckham-Nilsson answer-extraction algorithm  has been

implemented.  It is not  available  as part of the basic  prover, but

must be loaded by the user.  The prover should run in   slightly more

core to accommodate the answer routines.

Here is an example:
Recall example 2. in the introduction:

(1) ∀(x,y)P(x,y)∧P(y,z)⊃G(x,z)
(2) ∀y∃xP(x,y)
Question:(3) ∃(x,y)G(x,y) .

From the semantics of the problem we know that the "answer" to (3) is

"yes" and in fact we  can display specific solutions to  the problem:

The parent of the parent   is the grandparent.  What does  the answer

extractor do with this problem?

RU DSK PROVER[P,JRA]    ;get the prover
(DSKIN (P,JRA) ANSWER)  ;load in answer extractor 
(PROVE DSK: EX1)        
    ...
[output as before]
    ...
*(ANSPRED)              ;this calls the extractor
*G(G21(G21(x)),x)       ;the answer
*

We must now interpret  the Skolem function, G21.  G21  was introduced

in the  translation of (2),  that is, G21(y)  is an object  such that

P(G21(y),y).   Thus G21  is a  function to  select the  parent  of an

individual.   In  this  light our  answer,  G(G21(G21(x)),x),  is the

expected result.

The  current  implementation   of  the  answer  extractor   does  not



recognize  applications of  the equality  rule and  will fail  to get

answers in this case.  It is trivial to extend the algorithm  and its

implementation will occur shortly.



Appendix.  The Syntax Equations for the Theorem Prover.

The parsers for  the input syntax and  the command language  are both

contstructed by Lynn Quam's Syntax Directed Input Output program.

A-I.  THE INPUT FORMAT

The usual  form for input  consists of the  declarations of  the non-

logical  constituents  of  the  axioms,  followed  by  a  sequence of

statements.  The statements may be assigned names, and if a statement

whose name is the same as the current value of THEOREMNAME is present

that statement  is negated before  being added to  the memory  of the

prover.
<INPUT> ::=<DECOP>:<OPLIST>;
        ::=<ID>:
        ::=<STATEMENT>

<DECOP> ::=VAR | INF_OP | INF_PRED | PRE_OP | PRE_PRED | EQUALITY

<OPLIST>::=<OP>,<OPLIST>
        ::=<OP>

<STATEMENT>     ::=;
        ::=<S1>;

<S1>    ::=<S2>
        ::=<S1><EQUIV><S2>

<S2>    ::=<S3>
        ::=<S2><IMP><S3>

<S3>    ::=<S4>
        ::=<S3><OR><S4>

<S4>    ::=<S5>
        ::=<S4><AND><S5>

<S5>    ::=(<S1>)
        ::=<NOT><S5>
        ::=<QFF><BODY>
        ::=<PRED>



<BODY>  ::= <IVAR><S5>
        ::=(<VARLIST>)<S5>

<VARLIST>::=<IVAR>,<VARLIST>
        ::=<IVAR>

In   the  following,the   routines  corresponding   to  <PREPREDLET>,

<INFPREDLET>, <IVAR>, <PREFN>, and <INFN> check the lists  of prefix-

and infix- predicate and function letters, and the variable list, all

of which were manufactured by the appropriate declarations.

<PRED>  ::=<PREPREDLET><ITMLST>
        ::=<TM><INFPREDLET><TM>

<ITMLST>::=(<ITMS>)

<ITMS>  ::=<TM>,<ITMS>
        ::=<TM>

<TM>    ::=<IVAR>
        ::=<PREFN><ITMLST>
        ::=<PREFN>
        ::=(<TM>)
        ::=<TM><INFN><TM>


The logical connectives are defined as follows:

<EQUIV> ::= ≡ | ↔ 

<IMP>   ::= ⊃

<OR>    ::= ∨

<AND>   ::= ∧

<NOT>   ::= ¬

<QFF>   ::= ∀ | ∃



A-II. THE SIMPLE STRATEGY LANGUAGE

The most straightforwrd application of the strategy language consists

of using Boolean combinations of the builtin strategies.

<STRATEGY>::=<F1>;

<F1>    ::=<F2>
        ::=<F1><OR><F2>

<F2>    ::=<F3>
        ::=<F2><AND><F3>

<F3>    ::=(<F1>)
        ::=<NOT><F3>
        ::=<PREDIC>

<PREDIC>::=ANCESTRY
        ::=NONE
        ::=VINE
        ::=UNIT
        ::=P1
        ::=SUPPORT[<C>]
        ::=MODEL[<PREDLST>;<PREDLST>]
        ::=EQUALITY[<OP>;<NUMBER>]
        ::=DEMOD[<CLAUSES><NUMBER>]
        ::=DEFMODEL[ID]
        ::=LENGTH[<NUMBER>]
        ::=DEPTH[<NUMBER>]
        ::=SELDEPTH[<FNLST>]
        ::=<MPRM>

<PREDLST>
        ::=<ID>,<PREDLST>
        ::=<ID>
        ::=

<FNLST> ::= <FP>;<FNLST>
        ::= <FP>

<FP>    ::=<OP>,<NUMBER>



A-III.  THE COMMAND LANGUAGE



<CLAUSES> ::= <C>,<CLAUSES>
        ::= <C>

<C>     ::= @<STATEMENT>
        ::= DSK: <FILE>
        ::= <NUMBER>
        ::= <ID>[<VARLIST>]
        ::= <ID>
        ::= FIND [<ID>,<MATCH>]
        ::= FINDC [<MATCH>]

<FILE>  ::= <ID>
        ::= (<ID>.<ID>)

<VARLIST> ::= <NUMBER>,<VARLIST>
        ::= <NUMBER>

<COMMAND ::= AB <CLAUSES>;      ABandon proof attempt
        ::= AB;
        ::= AD <CLAUSES>;       ADd clauses to clauselist.

        ::= AN <CLAUSES>;       display ANcestry

        ::= CH;                 CHange strategies
        ::= CL <ID>;            Clear name from symbol table
        ::= CO;                 COntinue with proof search
        ::= CU;                 display CUrrent strategies

        ::= DE <CLAUSES>;       DElete clauses
        ::= DI <CLAUSES>;       DIsplay clauses
        ::= DO <NUMBER>;        move DOwn
        ::= DS <FILE>;          set output to DSk(see EOf)

        ::= EO;                 make End Of File
        ::= EV;                 enter Lisp's EVAL
                                  (leave via @END)
        ::= EX;                 EXecute subproof with 
                                   standard strategies.
        ::= FD;                 Float Down clause list
        ::= FU;                 Float Up clause list

        ::= GO <NUMBER>;        GO to designated clause
        ::= HA;                 HAlt to prover
        ::= HE;                 type HElp message




        ::= PA <CLAUSES>;CLAUSES>; PAramodulate selected 
                                     clauses.
        ::= PR <CLAUSES>;       Initialize subproof
                                  (see US,EX,and TR.)
        ::= RE <CLAUSES>;<CLAUSES>; REsolve clauses

        ::= SE <ID> <CLAUSES>;  SEt id as name for clauses.
        ::= SI <CLAUSES>; BY <CLAUSES>; SImplify
        ::= SU <TM> FOR <TM> IN <CLAUSES>; SUbstitute.
                                             (add to ASSERT)
        ::= SY;                 display current SYmbol table.

        ::= TE <CLAUSES>;       TErminate; (see Sec. 2-IV).
        ::= TE;
        ::= TR;                 TRies subproof with user's
                                   strategies.

        ::= UP <NUMBER>;        move UP  n clauses.



A-IV. THE MATCHER

<MATCH> ::= <M2>
        ::=<MATCH> ∨ <M2>

<M2>    ::= <M3>
        ::= <M2> ∧ <M3>

<M3>    ::= (<F1>)
        ::=¬<M3>
        ::=<MPRM>

<MPRM>  ::= <ARG><MOP><ARG1>

        ::= OCR[<PAT>]
        ::=TREE[<CNAME>]

<MOP>   ::= =
        ::= <
        ::= >

<ARG1> ::= <ARG>

<ARG>   ::= LENGTH
        ::=DEPTH
        ::=<NUMBER>

<CNAME> ::= <NUMBER>
        ::= <ID>[<VARLIST>]
        ::= <ID>

<PAT>   ::= <NOT><PRED>
        ::=<PRED>
        ::=<TM>
        ::=<FNLET>